(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, s(0), Y).
log2(s(s(X)), Half, Acc, Y) :- log2(X, s(Half), Acc, Y).
log2(X, s(s(Half)), Acc, Y) :- ','(small(X), log2(Half, s(0), s(Acc), Y)).
log2(X, Half, Y, Y) :- ','(small(X), small(Half)).
small(0).
small(s(0)).

Query: log2(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

log2A(s(s(X1)), X2, X3) :- log2A(X1, s(X2), X3).
log2A(0, s(X1), X2) :- log2B(X1, X2).
log2A(s(0), s(X1), X2) :- log2B(X1, X2).
log2C(s(s(X1)), X2, X3) :- log2C(X1, s(X2), X3).
log2C(0, s(X1), X2) :- log2D(X1, X2).
log2C(s(0), s(X1), X2) :- log2D(X1, X2).
log2E(s(s(X1)), X2, X3) :- log2E(X1, s(X2), X3).
log2E(0, s(X1), X2) :- log2F(X1, X2).
log2E(s(0), s(X1), X2) :- log2F(X1, X2).
log2G(s(s(X1)), X2, X3) :- log2G(X1, s(X2), X3).
log2G(0, s(X1), X2) :- log2H(X1, X2).
log2G(s(0), s(X1), X2) :- log2H(X1, X2).
log2I(s(s(X1)), X2, X3) :- log2I(X1, s(X2), X3).
log2I(0, s(X1), X2) :- log2J(X1, X2).
log2I(s(0), s(X1), X2) :- log2J(X1, X2).
log2K(s(s(X1)), X2, X3) :- log2K(X1, s(X2), X3).
log2K(0, s(X1), X2) :- log2L(X1, X2).
log2K(s(0), s(X1), X2) :- log2L(X1, X2).
log2M(s(s(X1)), X2, X3) :- log2M(X1, s(X2), X3).
log2M(0, s(X1), X2) :- log2N(X1, s(s(s(s(s(s(s(0))))))), X2).
log2M(s(0), s(X1), X2) :- log2N(X1, s(s(s(s(s(s(s(0))))))), X2).
log2O(s(s(X1)), X2, X3, X4) :- log2O(X1, s(X2), X3, X4).
log2O(0, s(X1), X2, X3) :- log2N(X1, s(X2), X3).
log2O(s(0), s(X1), X2, X3) :- log2N(X1, s(X2), X3).
log2N(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) :- log2O(X1, s(s(s(s(s(s(s(0))))))), X2, X3).
log2N(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1, X2) :- log2P(X1, X2).
log2N(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1, X2) :- log2P(X1, X2).
log2N(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1, X2) :- log2Q(X1, X2).
log2N(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1, X2) :- log2Q(X1, X2).
log2N(s(s(s(s(s(s(s(s(0)))))))), X1, X2) :- log2R(X1, X2).
log2N(s(s(s(s(s(s(s(s(s(0))))))))), X1, X2) :- log2R(X1, X2).
log2N(s(s(s(s(s(s(0)))))), X1, X2) :- log2S(X1, X2).
log2N(s(s(s(s(s(s(s(0))))))), X1, X2) :- log2S(X1, X2).
log2N(s(s(s(s(0)))), X1, X2) :- log2T(X1, X2).
log2N(s(s(s(s(s(0))))), X1, X2) :- log2T(X1, X2).
log2N(s(s(0)), X1, X2) :- log2U(X1, X2).
log2N(s(s(s(0))), X1, X2) :- log2U(X1, X2).
log2P(X1, X2) :- log2V(X1, X2).
log2Q(X1, X2) :- log2V(X1, X2).
log2R(X1, X2) :- log2W(X1, X2).
log2S(X1, X2) :- log2W(X1, X2).
log2X(X1, X2) :- log2T(X1, X2).
log2Y(X1, X2) :- log2T(X1, X2).
log2Z(X1, X2) :- log2U(X1, X2).
log2N1(X1, X2) :- log2U(X1, X2).
log2L(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2M(X1, s(s(s(s(s(s(s(0))))))), X2).
log2L(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2X(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2X(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2Y(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2Y(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2Z(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2Z(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(0)))))), X1) :- log2N1(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(s(s(0))))))), X1) :- log2N1(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(0)))), X1) :- log2N2(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(s(s(0))))), X1) :- log2N2(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(0)), X1) :- log2N3(s(s(s(s(s(s(s(0))))))), X1).
log2L(s(s(s(0))), X1) :- log2N3(s(s(s(s(s(s(s(0))))))), X1).
log2N4(X1) :- log2N2(s(s(s(s(s(s(s(0))))))), X1).
log2N5(X1) :- log2N2(s(s(s(s(s(s(s(0))))))), X1).
log2N6(X1) :- log2N3(s(s(s(s(s(s(s(0))))))), X1).
log2N7(X1) :- log2N3(s(s(s(s(s(s(s(0))))))), X1).
log2J(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2K(X1, s(s(s(s(s(s(s(0))))))), X2).
log2J(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N4(X1).
log2J(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N4(X1).
log2J(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N5(X1).
log2J(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N5(X1).
log2J(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N6(X1).
log2J(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N6(X1).
log2J(s(s(s(s(s(s(0)))))), X1) :- log2N7(X1).
log2J(s(s(s(s(s(s(s(0))))))), X1) :- log2N7(X1).
log2J(s(s(s(s(0)))), X1) :- log2N8(X1).
log2J(s(s(s(s(s(0))))), X1) :- log2N8(X1).
log2J(s(s(0)), X1) :- log2N9(X1).
log2J(s(s(s(0))), X1) :- log2N9(X1).
log2N10(X1) :- log2N8(X1).
log2N11(X1) :- log2N8(X1).
log2N12(X1) :- log2N9(X1).
log2N13(X1) :- log2N9(X1).
log2H(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2I(X1, s(s(s(s(s(s(s(0))))))), X2).
log2H(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N10(X1).
log2H(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N10(X1).
log2H(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N11(X1).
log2H(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N11(X1).
log2H(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N12(X1).
log2H(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N12(X1).
log2H(s(s(s(s(s(s(0)))))), X1) :- log2N13(X1).
log2H(s(s(s(s(s(s(s(0))))))), X1) :- log2N13(X1).
log2H(s(s(s(s(0)))), X1) :- log2N14(X1).
log2H(s(s(s(s(s(0))))), X1) :- log2N14(X1).
log2H(s(s(0)), X1) :- log2N15(X1).
log2H(s(s(s(0))), X1) :- log2N15(X1).
log2N16(X1) :- log2N14(X1).
log2N17(X1) :- log2N14(X1).
log2N18(X1) :- log2N15(X1).
log2N19(X1) :- log2N15(X1).
log2F(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2G(X1, s(s(s(s(s(s(s(0))))))), X2).
log2F(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N16(X1).
log2F(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N16(X1).
log2F(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N17(X1).
log2F(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N17(X1).
log2F(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N18(X1).
log2F(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N18(X1).
log2F(s(s(s(s(s(s(0)))))), X1) :- log2N19(X1).
log2F(s(s(s(s(s(s(s(0))))))), X1) :- log2N19(X1).
log2F(s(s(s(s(0)))), X1) :- log2N20(X1).
log2F(s(s(s(s(s(0))))), X1) :- log2N20(X1).
log2F(s(s(0)), X1) :- log2N21(X1).
log2F(s(s(s(0))), X1) :- log2N21(X1).
log2N22(X1) :- log2N20(X1).
log2N23(X1) :- log2N20(X1).
log2N24(X1) :- log2N21(X1).
log2N25(X1) :- log2N21(X1).
log2D(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2E(X1, s(s(s(s(s(s(s(0))))))), X2).
log2D(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N22(X1).
log2D(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N22(X1).
log2D(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N23(X1).
log2D(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N23(X1).
log2D(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N24(X1).
log2D(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N24(X1).
log2D(s(s(s(s(s(s(0)))))), X1) :- log2N25(X1).
log2D(s(s(s(s(s(s(s(0))))))), X1) :- log2N25(X1).
log2D(s(s(s(s(0)))), X1) :- log2N26(X1).
log2D(s(s(s(s(s(0))))), X1) :- log2N26(X1).
log2D(s(s(0)), X1) :- log2N27(X1).
log2D(s(s(s(0))), X1) :- log2N27(X1).
log2N28(X1) :- log2N26(X1).
log2N29(X1) :- log2N26(X1).
log2N30(X1) :- log2N27(X1).
log2N31(X1) :- log2N27(X1).
log2B(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2C(X1, s(s(s(s(s(s(s(0))))))), X2).
log2B(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N28(X1).
log2B(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N28(X1).
log2B(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N29(X1).
log2B(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N29(X1).
log2B(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N30(X1).
log2B(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N30(X1).
log2B(s(s(s(s(s(s(0)))))), X1) :- log2N31(X1).
log2B(s(s(s(s(s(s(s(0))))))), X1) :- log2N31(X1).
log2B(s(s(s(s(0)))), X1) :- log2N32(X1).
log2B(s(s(s(s(s(0))))), X1) :- log2N32(X1).
log2B(s(s(0)), X1) :- log2N33(X1).
log2B(s(s(s(0))), X1) :- log2N33(X1).
log2N34(X1) :- log2N32(X1).
log2N35(X1) :- log2N32(X1).
log2N36(X1) :- log2N33(X1).
log2N37(X1) :- log2N33(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) :- log2A(X1, s(s(s(s(s(s(s(0))))))), X2).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))), X1) :- log2N34(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))), X1) :- log2N34(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2N35(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2N35(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2N36(X1).
log2N40(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2N36(X1).
log2N40(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2N37(X1).
log2N40(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2N37(X1).
log2N40(s(s(s(s(s(s(0)))))), X1) :- log2N38(X1).
log2N40(s(s(s(s(s(s(s(0))))))), X1) :- log2N38(X1).
log2N40(s(s(s(s(0)))), X1) :- log2N39(X1).
log2N40(s(s(s(s(s(0))))), X1) :- log2N39(X1).

Clauses:

log2cA(s(s(X1)), X2, X3) :- log2cA(X1, s(X2), X3).
log2cA(0, s(X1), X2) :- log2cB(X1, X2).
log2cA(s(0), s(X1), X2) :- log2cB(X1, X2).
log2cA(0, 0, s(0)).
log2cA(s(0), 0, s(0)).
log2cC(s(s(X1)), X2, X3) :- log2cC(X1, s(X2), X3).
log2cC(0, s(X1), X2) :- log2cD(X1, X2).
log2cC(s(0), s(X1), X2) :- log2cD(X1, X2).
log2cC(0, 0, s(s(0))).
log2cC(s(0), 0, s(s(0))).
log2cE(s(s(X1)), X2, X3) :- log2cE(X1, s(X2), X3).
log2cE(0, s(X1), X2) :- log2cF(X1, X2).
log2cE(s(0), s(X1), X2) :- log2cF(X1, X2).
log2cE(0, 0, s(s(s(0)))).
log2cE(s(0), 0, s(s(s(0)))).
log2cG(s(s(X1)), X2, X3) :- log2cG(X1, s(X2), X3).
log2cG(0, s(X1), X2) :- log2cH(X1, X2).
log2cG(s(0), s(X1), X2) :- log2cH(X1, X2).
log2cG(0, 0, s(s(s(s(0))))).
log2cG(s(0), 0, s(s(s(s(0))))).
log2cI(s(s(X1)), X2, X3) :- log2cI(X1, s(X2), X3).
log2cI(0, s(X1), X2) :- log2cJ(X1, X2).
log2cI(s(0), s(X1), X2) :- log2cJ(X1, X2).
log2cI(0, 0, s(s(s(s(s(0)))))).
log2cI(s(0), 0, s(s(s(s(s(0)))))).
log2cK(s(s(X1)), X2, X3) :- log2cK(X1, s(X2), X3).
log2cK(0, s(X1), X2) :- log2cL(X1, X2).
log2cK(s(0), s(X1), X2) :- log2cL(X1, X2).
log2cK(0, 0, s(s(s(s(s(s(0))))))).
log2cK(s(0), 0, s(s(s(s(s(s(0))))))).
log2cM(s(s(X1)), X2, X3) :- log2cM(X1, s(X2), X3).
log2cM(0, s(X1), X2) :- log2cN(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cM(s(0), s(X1), X2) :- log2cN(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cM(0, 0, s(s(s(s(s(s(s(0)))))))).
log2cM(s(0), 0, s(s(s(s(s(s(s(0)))))))).
log2cO(s(s(X1)), X2, X3, X4) :- log2cO(X1, s(X2), X3, X4).
log2cO(0, s(X1), X2, X3) :- log2cN(X1, s(X2), X3).
log2cO(s(0), s(X1), X2, X3) :- log2cN(X1, s(X2), X3).
log2cO(0, 0, X1, s(X1)).
log2cO(s(0), 0, X1, s(X1)).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) :- log2cO(X1, s(s(s(s(s(s(s(0))))))), X2, X3).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1, X2) :- log2cP(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1, X2) :- log2cP(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1, X2) :- log2cQ(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1, X2) :- log2cQ(X1, X2).
log2cN(s(s(s(s(s(s(s(s(0)))))))), X1, X2) :- log2cR(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(0))))))))), X1, X2) :- log2cR(X1, X2).
log2cN(s(s(s(s(s(s(0)))))), X1, X2) :- log2cS(X1, X2).
log2cN(s(s(s(s(s(s(s(0))))))), X1, X2) :- log2cS(X1, X2).
log2cN(s(s(s(s(0)))), X1, X2) :- log2cT(X1, X2).
log2cN(s(s(s(s(s(0))))), X1, X2) :- log2cT(X1, X2).
log2cN(s(s(0)), X1, X2) :- log2cU(X1, X2).
log2cN(s(s(s(0))), X1, X2) :- log2cU(X1, X2).
log2cN(0, X1, s(X1)).
log2cN(s(0), X1, s(X1)).
log2cP(X1, X2) :- log2cV(X1, X2).
log2cV(X1, s(s(s(X1)))).
log2cQ(X1, X2) :- log2cV(X1, X2).
log2cR(X1, X2) :- log2cW(X1, X2).
log2cW(X1, s(s(s(X1)))).
log2cS(X1, X2) :- log2cW(X1, X2).
log2cT(X1, s(s(X1))).
log2cU(X1, s(s(X1))).
log2cX(X1, X2) :- log2cT(X1, X2).
log2cY(X1, X2) :- log2cT(X1, X2).
log2cZ(X1, X2) :- log2cU(X1, X2).
log2cN1(X1, X2) :- log2cU(X1, X2).
log2cN2(X1, s(X1)).
log2cN3(X1, s(X1)).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cM(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cX(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cX(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cY(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cY(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cZ(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cZ(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(0)))))), X1) :- log2cN1(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(0))))))), X1) :- log2cN1(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(0)))), X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(0))))), X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(0)), X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(0))), X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cL(0, s(s(s(s(s(s(s(0)))))))).
log2cL(s(0), s(s(s(s(s(s(s(0)))))))).
log2cN4(X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cN5(X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cN6(X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cN7(X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cN8(s(s(s(s(s(s(s(0)))))))).
log2cN9(s(s(s(s(s(s(s(0)))))))).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cK(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN4(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN4(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN5(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN5(X1).
log2cJ(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN6(X1).
log2cJ(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN6(X1).
log2cJ(s(s(s(s(s(s(0)))))), X1) :- log2cN7(X1).
log2cJ(s(s(s(s(s(s(s(0))))))), X1) :- log2cN7(X1).
log2cJ(s(s(s(s(0)))), X1) :- log2cN8(X1).
log2cJ(s(s(s(s(s(0))))), X1) :- log2cN8(X1).
log2cJ(s(s(0)), X1) :- log2cN9(X1).
log2cJ(s(s(s(0))), X1) :- log2cN9(X1).
log2cJ(0, s(s(s(s(s(s(0))))))).
log2cJ(s(0), s(s(s(s(s(s(0))))))).
log2cN10(X1) :- log2cN8(X1).
log2cN11(X1) :- log2cN8(X1).
log2cN12(X1) :- log2cN9(X1).
log2cN13(X1) :- log2cN9(X1).
log2cN14(s(s(s(s(s(s(0))))))).
log2cN15(s(s(s(s(s(s(0))))))).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cI(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN10(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN10(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN11(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN11(X1).
log2cH(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN12(X1).
log2cH(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN12(X1).
log2cH(s(s(s(s(s(s(0)))))), X1) :- log2cN13(X1).
log2cH(s(s(s(s(s(s(s(0))))))), X1) :- log2cN13(X1).
log2cH(s(s(s(s(0)))), X1) :- log2cN14(X1).
log2cH(s(s(s(s(s(0))))), X1) :- log2cN14(X1).
log2cH(s(s(0)), X1) :- log2cN15(X1).
log2cH(s(s(s(0))), X1) :- log2cN15(X1).
log2cH(0, s(s(s(s(s(0)))))).
log2cH(s(0), s(s(s(s(s(0)))))).
log2cN16(X1) :- log2cN14(X1).
log2cN17(X1) :- log2cN14(X1).
log2cN18(X1) :- log2cN15(X1).
log2cN19(X1) :- log2cN15(X1).
log2cN20(s(s(s(s(s(0)))))).
log2cN21(s(s(s(s(s(0)))))).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cG(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN16(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN16(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN17(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN17(X1).
log2cF(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN18(X1).
log2cF(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN18(X1).
log2cF(s(s(s(s(s(s(0)))))), X1) :- log2cN19(X1).
log2cF(s(s(s(s(s(s(s(0))))))), X1) :- log2cN19(X1).
log2cF(s(s(s(s(0)))), X1) :- log2cN20(X1).
log2cF(s(s(s(s(s(0))))), X1) :- log2cN20(X1).
log2cF(s(s(0)), X1) :- log2cN21(X1).
log2cF(s(s(s(0))), X1) :- log2cN21(X1).
log2cF(0, s(s(s(s(0))))).
log2cF(s(0), s(s(s(s(0))))).
log2cN22(X1) :- log2cN20(X1).
log2cN23(X1) :- log2cN20(X1).
log2cN24(X1) :- log2cN21(X1).
log2cN25(X1) :- log2cN21(X1).
log2cN26(s(s(s(s(0))))).
log2cN27(s(s(s(s(0))))).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cE(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN22(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN22(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN23(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN23(X1).
log2cD(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN24(X1).
log2cD(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN24(X1).
log2cD(s(s(s(s(s(s(0)))))), X1) :- log2cN25(X1).
log2cD(s(s(s(s(s(s(s(0))))))), X1) :- log2cN25(X1).
log2cD(s(s(s(s(0)))), X1) :- log2cN26(X1).
log2cD(s(s(s(s(s(0))))), X1) :- log2cN26(X1).
log2cD(s(s(0)), X1) :- log2cN27(X1).
log2cD(s(s(s(0))), X1) :- log2cN27(X1).
log2cD(0, s(s(s(0)))).
log2cD(s(0), s(s(s(0)))).
log2cN28(X1) :- log2cN26(X1).
log2cN29(X1) :- log2cN26(X1).
log2cN30(X1) :- log2cN27(X1).
log2cN31(X1) :- log2cN27(X1).
log2cN32(s(s(s(0)))).
log2cN33(s(s(s(0)))).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cC(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN28(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN28(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN29(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN29(X1).
log2cB(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN30(X1).
log2cB(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN30(X1).
log2cB(s(s(s(s(s(s(0)))))), X1) :- log2cN31(X1).
log2cB(s(s(s(s(s(s(s(0))))))), X1) :- log2cN31(X1).
log2cB(s(s(s(s(0)))), X1) :- log2cN32(X1).
log2cB(s(s(s(s(s(0))))), X1) :- log2cN32(X1).
log2cB(s(s(0)), X1) :- log2cN33(X1).
log2cB(s(s(s(0))), X1) :- log2cN33(X1).
log2cB(0, s(s(0))).
log2cB(s(0), s(s(0))).
log2cN34(X1) :- log2cN32(X1).
log2cN35(X1) :- log2cN32(X1).
log2cN36(X1) :- log2cN33(X1).
log2cN37(X1) :- log2cN33(X1).
log2cN38(s(s(0))).
log2cN39(s(s(0))).

Afs:

log2N40(x1, x2)  =  log2N40(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

log2A(s(s(X1)), X2, X3) :- log2A(X1, s(X2), X3).
log2A(0, s(X1), X2) :- log2B(X1, X2).
log2A(s(0), s(X1), X2) :- log2B(X1, X2).
log2C(s(s(X1)), X2, X3) :- log2C(X1, s(X2), X3).
log2C(0, s(X1), X2) :- log2D(X1, X2).
log2C(s(0), s(X1), X2) :- log2D(X1, X2).
log2E(s(s(X1)), X2, X3) :- log2E(X1, s(X2), X3).
log2E(0, s(X1), X2) :- log2F(X1, X2).
log2E(s(0), s(X1), X2) :- log2F(X1, X2).
log2G(s(s(X1)), X2, X3) :- log2G(X1, s(X2), X3).
log2G(0, s(X1), X2) :- log2H(X1, X2).
log2G(s(0), s(X1), X2) :- log2H(X1, X2).
log2I(s(s(X1)), X2, X3) :- log2I(X1, s(X2), X3).
log2I(0, s(X1), X2) :- log2J(X1, X2).
log2I(s(0), s(X1), X2) :- log2J(X1, X2).
log2K(s(s(X1)), X2, X3) :- log2K(X1, s(X2), X3).
log2K(0, s(X1), X2) :- log2L(X1, X2).
log2K(s(0), s(X1), X2) :- log2L(X1, X2).
log2M(s(s(X1)), X2, X3) :- log2M(X1, s(X2), X3).
log2M(0, s(X1), X2) :- log2N(X1, s(s(s(s(s(s(s(0))))))), X2).
log2M(s(0), s(X1), X2) :- log2N(X1, s(s(s(s(s(s(s(0))))))), X2).
log2O(s(s(X1)), X2, X3, X4) :- log2O(X1, s(X2), X3, X4).
log2O(0, s(X1), X2, X3) :- log2N(X1, s(X2), X3).
log2O(s(0), s(X1), X2, X3) :- log2N(X1, s(X2), X3).
log2N(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) :- log2O(X1, s(s(s(s(s(s(s(0))))))), X2, X3).
log2L(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2M(X1, s(s(s(s(s(s(s(0))))))), X2).
log2J(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2K(X1, s(s(s(s(s(s(s(0))))))), X2).
log2H(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2I(X1, s(s(s(s(s(s(s(0))))))), X2).
log2F(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2G(X1, s(s(s(s(s(s(s(0))))))), X2).
log2D(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2E(X1, s(s(s(s(s(s(s(0))))))), X2).
log2B(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2C(X1, s(s(s(s(s(s(s(0))))))), X2).
log2N40(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) :- log2A(X1, s(s(s(s(s(s(s(0))))))), X2).

Clauses:

log2cA(s(s(X1)), X2, X3) :- log2cA(X1, s(X2), X3).
log2cA(0, s(X1), X2) :- log2cB(X1, X2).
log2cA(s(0), s(X1), X2) :- log2cB(X1, X2).
log2cA(0, 0, s(0)).
log2cA(s(0), 0, s(0)).
log2cC(s(s(X1)), X2, X3) :- log2cC(X1, s(X2), X3).
log2cC(0, s(X1), X2) :- log2cD(X1, X2).
log2cC(s(0), s(X1), X2) :- log2cD(X1, X2).
log2cC(0, 0, s(s(0))).
log2cC(s(0), 0, s(s(0))).
log2cE(s(s(X1)), X2, X3) :- log2cE(X1, s(X2), X3).
log2cE(0, s(X1), X2) :- log2cF(X1, X2).
log2cE(s(0), s(X1), X2) :- log2cF(X1, X2).
log2cE(0, 0, s(s(s(0)))).
log2cE(s(0), 0, s(s(s(0)))).
log2cG(s(s(X1)), X2, X3) :- log2cG(X1, s(X2), X3).
log2cG(0, s(X1), X2) :- log2cH(X1, X2).
log2cG(s(0), s(X1), X2) :- log2cH(X1, X2).
log2cG(0, 0, s(s(s(s(0))))).
log2cG(s(0), 0, s(s(s(s(0))))).
log2cI(s(s(X1)), X2, X3) :- log2cI(X1, s(X2), X3).
log2cI(0, s(X1), X2) :- log2cJ(X1, X2).
log2cI(s(0), s(X1), X2) :- log2cJ(X1, X2).
log2cI(0, 0, s(s(s(s(s(0)))))).
log2cI(s(0), 0, s(s(s(s(s(0)))))).
log2cK(s(s(X1)), X2, X3) :- log2cK(X1, s(X2), X3).
log2cK(0, s(X1), X2) :- log2cL(X1, X2).
log2cK(s(0), s(X1), X2) :- log2cL(X1, X2).
log2cK(0, 0, s(s(s(s(s(s(0))))))).
log2cK(s(0), 0, s(s(s(s(s(s(0))))))).
log2cM(s(s(X1)), X2, X3) :- log2cM(X1, s(X2), X3).
log2cM(0, s(X1), X2) :- log2cN(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cM(s(0), s(X1), X2) :- log2cN(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cM(0, 0, s(s(s(s(s(s(s(0)))))))).
log2cM(s(0), 0, s(s(s(s(s(s(s(0)))))))).
log2cO(s(s(X1)), X2, X3, X4) :- log2cO(X1, s(X2), X3, X4).
log2cO(0, s(X1), X2, X3) :- log2cN(X1, s(X2), X3).
log2cO(s(0), s(X1), X2, X3) :- log2cN(X1, s(X2), X3).
log2cO(0, 0, X1, s(X1)).
log2cO(s(0), 0, X1, s(X1)).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) :- log2cO(X1, s(s(s(s(s(s(s(0))))))), X2, X3).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1, X2) :- log2cP(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1, X2) :- log2cP(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1, X2) :- log2cQ(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1, X2) :- log2cQ(X1, X2).
log2cN(s(s(s(s(s(s(s(s(0)))))))), X1, X2) :- log2cR(X1, X2).
log2cN(s(s(s(s(s(s(s(s(s(0))))))))), X1, X2) :- log2cR(X1, X2).
log2cN(s(s(s(s(s(s(0)))))), X1, X2) :- log2cS(X1, X2).
log2cN(s(s(s(s(s(s(s(0))))))), X1, X2) :- log2cS(X1, X2).
log2cN(s(s(s(s(0)))), X1, X2) :- log2cT(X1, X2).
log2cN(s(s(s(s(s(0))))), X1, X2) :- log2cT(X1, X2).
log2cN(s(s(0)), X1, X2) :- log2cU(X1, X2).
log2cN(s(s(s(0))), X1, X2) :- log2cU(X1, X2).
log2cN(0, X1, s(X1)).
log2cN(s(0), X1, s(X1)).
log2cP(X1, X2) :- log2cV(X1, X2).
log2cV(X1, s(s(s(X1)))).
log2cQ(X1, X2) :- log2cV(X1, X2).
log2cR(X1, X2) :- log2cW(X1, X2).
log2cW(X1, s(s(s(X1)))).
log2cS(X1, X2) :- log2cW(X1, X2).
log2cT(X1, s(s(X1))).
log2cU(X1, s(s(X1))).
log2cX(X1, X2) :- log2cT(X1, X2).
log2cY(X1, X2) :- log2cT(X1, X2).
log2cZ(X1, X2) :- log2cU(X1, X2).
log2cN1(X1, X2) :- log2cU(X1, X2).
log2cN2(X1, s(X1)).
log2cN3(X1, s(X1)).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cM(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cX(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cX(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cY(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cY(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cZ(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cZ(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(0)))))), X1) :- log2cN1(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(s(s(0))))))), X1) :- log2cN1(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(0)))), X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(s(s(0))))), X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(0)), X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cL(s(s(s(0))), X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cL(0, s(s(s(s(s(s(s(0)))))))).
log2cL(s(0), s(s(s(s(s(s(s(0)))))))).
log2cN4(X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cN5(X1) :- log2cN2(s(s(s(s(s(s(s(0))))))), X1).
log2cN6(X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cN7(X1) :- log2cN3(s(s(s(s(s(s(s(0))))))), X1).
log2cN8(s(s(s(s(s(s(s(0)))))))).
log2cN9(s(s(s(s(s(s(s(0)))))))).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cK(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN4(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN4(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN5(X1).
log2cJ(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN5(X1).
log2cJ(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN6(X1).
log2cJ(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN6(X1).
log2cJ(s(s(s(s(s(s(0)))))), X1) :- log2cN7(X1).
log2cJ(s(s(s(s(s(s(s(0))))))), X1) :- log2cN7(X1).
log2cJ(s(s(s(s(0)))), X1) :- log2cN8(X1).
log2cJ(s(s(s(s(s(0))))), X1) :- log2cN8(X1).
log2cJ(s(s(0)), X1) :- log2cN9(X1).
log2cJ(s(s(s(0))), X1) :- log2cN9(X1).
log2cJ(0, s(s(s(s(s(s(0))))))).
log2cJ(s(0), s(s(s(s(s(s(0))))))).
log2cN10(X1) :- log2cN8(X1).
log2cN11(X1) :- log2cN8(X1).
log2cN12(X1) :- log2cN9(X1).
log2cN13(X1) :- log2cN9(X1).
log2cN14(s(s(s(s(s(s(0))))))).
log2cN15(s(s(s(s(s(s(0))))))).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cI(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN10(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN10(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN11(X1).
log2cH(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN11(X1).
log2cH(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN12(X1).
log2cH(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN12(X1).
log2cH(s(s(s(s(s(s(0)))))), X1) :- log2cN13(X1).
log2cH(s(s(s(s(s(s(s(0))))))), X1) :- log2cN13(X1).
log2cH(s(s(s(s(0)))), X1) :- log2cN14(X1).
log2cH(s(s(s(s(s(0))))), X1) :- log2cN14(X1).
log2cH(s(s(0)), X1) :- log2cN15(X1).
log2cH(s(s(s(0))), X1) :- log2cN15(X1).
log2cH(0, s(s(s(s(s(0)))))).
log2cH(s(0), s(s(s(s(s(0)))))).
log2cN16(X1) :- log2cN14(X1).
log2cN17(X1) :- log2cN14(X1).
log2cN18(X1) :- log2cN15(X1).
log2cN19(X1) :- log2cN15(X1).
log2cN20(s(s(s(s(s(0)))))).
log2cN21(s(s(s(s(s(0)))))).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cG(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN16(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN16(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN17(X1).
log2cF(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN17(X1).
log2cF(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN18(X1).
log2cF(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN18(X1).
log2cF(s(s(s(s(s(s(0)))))), X1) :- log2cN19(X1).
log2cF(s(s(s(s(s(s(s(0))))))), X1) :- log2cN19(X1).
log2cF(s(s(s(s(0)))), X1) :- log2cN20(X1).
log2cF(s(s(s(s(s(0))))), X1) :- log2cN20(X1).
log2cF(s(s(0)), X1) :- log2cN21(X1).
log2cF(s(s(s(0))), X1) :- log2cN21(X1).
log2cF(0, s(s(s(s(0))))).
log2cF(s(0), s(s(s(s(0))))).
log2cN22(X1) :- log2cN20(X1).
log2cN23(X1) :- log2cN20(X1).
log2cN24(X1) :- log2cN21(X1).
log2cN25(X1) :- log2cN21(X1).
log2cN26(s(s(s(s(0))))).
log2cN27(s(s(s(s(0))))).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cE(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN22(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN22(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN23(X1).
log2cD(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN23(X1).
log2cD(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN24(X1).
log2cD(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN24(X1).
log2cD(s(s(s(s(s(s(0)))))), X1) :- log2cN25(X1).
log2cD(s(s(s(s(s(s(s(0))))))), X1) :- log2cN25(X1).
log2cD(s(s(s(s(0)))), X1) :- log2cN26(X1).
log2cD(s(s(s(s(s(0))))), X1) :- log2cN26(X1).
log2cD(s(s(0)), X1) :- log2cN27(X1).
log2cD(s(s(s(0))), X1) :- log2cN27(X1).
log2cD(0, s(s(s(0)))).
log2cD(s(0), s(s(s(0)))).
log2cN28(X1) :- log2cN26(X1).
log2cN29(X1) :- log2cN26(X1).
log2cN30(X1) :- log2cN27(X1).
log2cN31(X1) :- log2cN27(X1).
log2cN32(s(s(s(0)))).
log2cN33(s(s(s(0)))).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) :- log2cC(X1, s(s(s(s(s(s(s(0))))))), X2).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), X1) :- log2cN28(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))), X1) :- log2cN28(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(0)))))))))), X1) :- log2cN29(X1).
log2cB(s(s(s(s(s(s(s(s(s(s(s(0))))))))))), X1) :- log2cN29(X1).
log2cB(s(s(s(s(s(s(s(s(0)))))))), X1) :- log2cN30(X1).
log2cB(s(s(s(s(s(s(s(s(s(0))))))))), X1) :- log2cN30(X1).
log2cB(s(s(s(s(s(s(0)))))), X1) :- log2cN31(X1).
log2cB(s(s(s(s(s(s(s(0))))))), X1) :- log2cN31(X1).
log2cB(s(s(s(s(0)))), X1) :- log2cN32(X1).
log2cB(s(s(s(s(s(0))))), X1) :- log2cN32(X1).
log2cB(s(s(0)), X1) :- log2cN33(X1).
log2cB(s(s(s(0))), X1) :- log2cN33(X1).
log2cB(0, s(s(0))).
log2cB(s(0), s(s(0))).
log2cN34(X1) :- log2cN32(X1).
log2cN35(X1) :- log2cN32(X1).
log2cN36(X1) :- log2cN33(X1).
log2cN37(X1) :- log2cN33(X1).
log2cN38(s(s(0))).
log2cN39(s(s(0))).

Afs:

log2N40(x1, x2)  =  log2N40(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
log2N40_in: (b,f)
log2A_in: (b,b,f)
log2B_in: (b,f)
log2C_in: (b,b,f)
log2D_in: (b,f)
log2E_in: (b,b,f)
log2F_in: (b,f)
log2G_in: (b,b,f)
log2H_in: (b,f)
log2I_in: (b,b,f)
log2J_in: (b,f)
log2K_in: (b,b,f)
log2L_in: (b,f)
log2M_in: (b,b,f)
log2N_in: (b,b,f)
log2O_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

LOG2N40_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) → U32_GA(X1, X2, log2A_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2N40_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) → LOG2A_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2A_IN_GGA(s(s(X1)), X2, X3) → U1_GGA(X1, X2, X3, log2A_in_gga(X1, s(X2), X3))
LOG2A_IN_GGA(s(s(X1)), X2, X3) → LOG2A_IN_GGA(X1, s(X2), X3)
LOG2A_IN_GGA(0, s(X1), X2) → U2_GGA(X1, X2, log2B_in_ga(X1, X2))
LOG2A_IN_GGA(0, s(X1), X2) → LOG2B_IN_GA(X1, X2)
LOG2B_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U31_GA(X1, X2, log2C_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2B_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2C_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2C_IN_GGA(s(s(X1)), X2, X3) → U4_GGA(X1, X2, X3, log2C_in_gga(X1, s(X2), X3))
LOG2C_IN_GGA(s(s(X1)), X2, X3) → LOG2C_IN_GGA(X1, s(X2), X3)
LOG2C_IN_GGA(0, s(X1), X2) → U5_GGA(X1, X2, log2D_in_ga(X1, X2))
LOG2C_IN_GGA(0, s(X1), X2) → LOG2D_IN_GA(X1, X2)
LOG2D_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U30_GA(X1, X2, log2E_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2D_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2E_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2E_IN_GGA(s(s(X1)), X2, X3) → U7_GGA(X1, X2, X3, log2E_in_gga(X1, s(X2), X3))
LOG2E_IN_GGA(s(s(X1)), X2, X3) → LOG2E_IN_GGA(X1, s(X2), X3)
LOG2E_IN_GGA(0, s(X1), X2) → U8_GGA(X1, X2, log2F_in_ga(X1, X2))
LOG2E_IN_GGA(0, s(X1), X2) → LOG2F_IN_GA(X1, X2)
LOG2F_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U29_GA(X1, X2, log2G_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2F_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2G_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2G_IN_GGA(s(s(X1)), X2, X3) → U10_GGA(X1, X2, X3, log2G_in_gga(X1, s(X2), X3))
LOG2G_IN_GGA(s(s(X1)), X2, X3) → LOG2G_IN_GGA(X1, s(X2), X3)
LOG2G_IN_GGA(0, s(X1), X2) → U11_GGA(X1, X2, log2H_in_ga(X1, X2))
LOG2G_IN_GGA(0, s(X1), X2) → LOG2H_IN_GA(X1, X2)
LOG2H_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U28_GA(X1, X2, log2I_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2H_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2I_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2I_IN_GGA(s(s(X1)), X2, X3) → U13_GGA(X1, X2, X3, log2I_in_gga(X1, s(X2), X3))
LOG2I_IN_GGA(s(s(X1)), X2, X3) → LOG2I_IN_GGA(X1, s(X2), X3)
LOG2I_IN_GGA(0, s(X1), X2) → U14_GGA(X1, X2, log2J_in_ga(X1, X2))
LOG2I_IN_GGA(0, s(X1), X2) → LOG2J_IN_GA(X1, X2)
LOG2J_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U27_GA(X1, X2, log2K_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2J_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2K_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2K_IN_GGA(s(s(X1)), X2, X3) → U16_GGA(X1, X2, X3, log2K_in_gga(X1, s(X2), X3))
LOG2K_IN_GGA(s(s(X1)), X2, X3) → LOG2K_IN_GGA(X1, s(X2), X3)
LOG2K_IN_GGA(0, s(X1), X2) → U17_GGA(X1, X2, log2L_in_ga(X1, X2))
LOG2K_IN_GGA(0, s(X1), X2) → LOG2L_IN_GA(X1, X2)
LOG2L_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U26_GA(X1, X2, log2M_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2L_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2M_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2M_IN_GGA(s(s(X1)), X2, X3) → U19_GGA(X1, X2, X3, log2M_in_gga(X1, s(X2), X3))
LOG2M_IN_GGA(s(s(X1)), X2, X3) → LOG2M_IN_GGA(X1, s(X2), X3)
LOG2M_IN_GGA(0, s(X1), X2) → U20_GGA(X1, X2, log2N_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2M_IN_GGA(0, s(X1), X2) → LOG2N_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) → U25_GGA(X1, X2, X3, log2O_in_ggga(X1, s(s(s(s(s(s(s(0))))))), X2, X3))
LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) → LOG2O_IN_GGGA(X1, s(s(s(s(s(s(s(0))))))), X2, X3)
LOG2O_IN_GGGA(s(s(X1)), X2, X3, X4) → U22_GGGA(X1, X2, X3, X4, log2O_in_ggga(X1, s(X2), X3, X4))
LOG2O_IN_GGGA(s(s(X1)), X2, X3, X4) → LOG2O_IN_GGGA(X1, s(X2), X3, X4)
LOG2O_IN_GGGA(0, s(X1), X2, X3) → U23_GGGA(X1, X2, X3, log2N_in_gga(X1, s(X2), X3))
LOG2O_IN_GGGA(0, s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)
LOG2O_IN_GGGA(s(0), s(X1), X2, X3) → U24_GGGA(X1, X2, X3, log2N_in_gga(X1, s(X2), X3))
LOG2O_IN_GGGA(s(0), s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)
LOG2M_IN_GGA(s(0), s(X1), X2) → U21_GGA(X1, X2, log2N_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2M_IN_GGA(s(0), s(X1), X2) → LOG2N_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2K_IN_GGA(s(0), s(X1), X2) → U18_GGA(X1, X2, log2L_in_ga(X1, X2))
LOG2K_IN_GGA(s(0), s(X1), X2) → LOG2L_IN_GA(X1, X2)
LOG2I_IN_GGA(s(0), s(X1), X2) → U15_GGA(X1, X2, log2J_in_ga(X1, X2))
LOG2I_IN_GGA(s(0), s(X1), X2) → LOG2J_IN_GA(X1, X2)
LOG2G_IN_GGA(s(0), s(X1), X2) → U12_GGA(X1, X2, log2H_in_ga(X1, X2))
LOG2G_IN_GGA(s(0), s(X1), X2) → LOG2H_IN_GA(X1, X2)
LOG2E_IN_GGA(s(0), s(X1), X2) → U9_GGA(X1, X2, log2F_in_ga(X1, X2))
LOG2E_IN_GGA(s(0), s(X1), X2) → LOG2F_IN_GA(X1, X2)
LOG2C_IN_GGA(s(0), s(X1), X2) → U6_GGA(X1, X2, log2D_in_ga(X1, X2))
LOG2C_IN_GGA(s(0), s(X1), X2) → LOG2D_IN_GA(X1, X2)
LOG2A_IN_GGA(s(0), s(X1), X2) → U3_GGA(X1, X2, log2B_in_ga(X1, X2))
LOG2A_IN_GGA(s(0), s(X1), X2) → LOG2B_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
log2A_in_gga(x1, x2, x3)  =  log2A_in_gga(x1, x2)
0  =  0
log2B_in_ga(x1, x2)  =  log2B_in_ga(x1)
log2C_in_gga(x1, x2, x3)  =  log2C_in_gga(x1, x2)
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
log2E_in_gga(x1, x2, x3)  =  log2E_in_gga(x1, x2)
log2F_in_ga(x1, x2)  =  log2F_in_ga(x1)
log2G_in_gga(x1, x2, x3)  =  log2G_in_gga(x1, x2)
log2H_in_ga(x1, x2)  =  log2H_in_ga(x1)
log2I_in_gga(x1, x2, x3)  =  log2I_in_gga(x1, x2)
log2J_in_ga(x1, x2)  =  log2J_in_ga(x1)
log2K_in_gga(x1, x2, x3)  =  log2K_in_gga(x1, x2)
log2L_in_ga(x1, x2)  =  log2L_in_ga(x1)
log2M_in_gga(x1, x2, x3)  =  log2M_in_gga(x1, x2)
log2N_in_gga(x1, x2, x3)  =  log2N_in_gga(x1, x2)
log2O_in_ggga(x1, x2, x3, x4)  =  log2O_in_ggga(x1, x2, x3)
LOG2N40_IN_GA(x1, x2)  =  LOG2N40_IN_GA(x1)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
LOG2A_IN_GGA(x1, x2, x3)  =  LOG2A_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3)  =  U2_GGA(x1, x3)
LOG2B_IN_GA(x1, x2)  =  LOG2B_IN_GA(x1)
U31_GA(x1, x2, x3)  =  U31_GA(x1, x3)
LOG2C_IN_GGA(x1, x2, x3)  =  LOG2C_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
LOG2D_IN_GA(x1, x2)  =  LOG2D_IN_GA(x1)
U30_GA(x1, x2, x3)  =  U30_GA(x1, x3)
LOG2E_IN_GGA(x1, x2, x3)  =  LOG2E_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
LOG2F_IN_GA(x1, x2)  =  LOG2F_IN_GA(x1)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
LOG2G_IN_GGA(x1, x2, x3)  =  LOG2G_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
LOG2H_IN_GA(x1, x2)  =  LOG2H_IN_GA(x1)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
LOG2I_IN_GGA(x1, x2, x3)  =  LOG2I_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
LOG2J_IN_GA(x1, x2)  =  LOG2J_IN_GA(x1)
U27_GA(x1, x2, x3)  =  U27_GA(x1, x3)
LOG2K_IN_GGA(x1, x2, x3)  =  LOG2K_IN_GGA(x1, x2)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
LOG2L_IN_GA(x1, x2)  =  LOG2L_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
LOG2M_IN_GGA(x1, x2, x3)  =  LOG2M_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
LOG2N_IN_GGA(x1, x2, x3)  =  LOG2N_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
LOG2O_IN_GGGA(x1, x2, x3, x4)  =  LOG2O_IN_GGGA(x1, x2, x3)
U22_GGGA(x1, x2, x3, x4, x5)  =  U22_GGGA(x1, x2, x3, x5)
U23_GGGA(x1, x2, x3, x4)  =  U23_GGGA(x1, x2, x4)
U24_GGGA(x1, x2, x3, x4)  =  U24_GGGA(x1, x2, x4)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2N40_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) → U32_GA(X1, X2, log2A_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2N40_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))), X2) → LOG2A_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2A_IN_GGA(s(s(X1)), X2, X3) → U1_GGA(X1, X2, X3, log2A_in_gga(X1, s(X2), X3))
LOG2A_IN_GGA(s(s(X1)), X2, X3) → LOG2A_IN_GGA(X1, s(X2), X3)
LOG2A_IN_GGA(0, s(X1), X2) → U2_GGA(X1, X2, log2B_in_ga(X1, X2))
LOG2A_IN_GGA(0, s(X1), X2) → LOG2B_IN_GA(X1, X2)
LOG2B_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U31_GA(X1, X2, log2C_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2B_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2C_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2C_IN_GGA(s(s(X1)), X2, X3) → U4_GGA(X1, X2, X3, log2C_in_gga(X1, s(X2), X3))
LOG2C_IN_GGA(s(s(X1)), X2, X3) → LOG2C_IN_GGA(X1, s(X2), X3)
LOG2C_IN_GGA(0, s(X1), X2) → U5_GGA(X1, X2, log2D_in_ga(X1, X2))
LOG2C_IN_GGA(0, s(X1), X2) → LOG2D_IN_GA(X1, X2)
LOG2D_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U30_GA(X1, X2, log2E_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2D_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2E_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2E_IN_GGA(s(s(X1)), X2, X3) → U7_GGA(X1, X2, X3, log2E_in_gga(X1, s(X2), X3))
LOG2E_IN_GGA(s(s(X1)), X2, X3) → LOG2E_IN_GGA(X1, s(X2), X3)
LOG2E_IN_GGA(0, s(X1), X2) → U8_GGA(X1, X2, log2F_in_ga(X1, X2))
LOG2E_IN_GGA(0, s(X1), X2) → LOG2F_IN_GA(X1, X2)
LOG2F_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U29_GA(X1, X2, log2G_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2F_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2G_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2G_IN_GGA(s(s(X1)), X2, X3) → U10_GGA(X1, X2, X3, log2G_in_gga(X1, s(X2), X3))
LOG2G_IN_GGA(s(s(X1)), X2, X3) → LOG2G_IN_GGA(X1, s(X2), X3)
LOG2G_IN_GGA(0, s(X1), X2) → U11_GGA(X1, X2, log2H_in_ga(X1, X2))
LOG2G_IN_GGA(0, s(X1), X2) → LOG2H_IN_GA(X1, X2)
LOG2H_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U28_GA(X1, X2, log2I_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2H_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2I_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2I_IN_GGA(s(s(X1)), X2, X3) → U13_GGA(X1, X2, X3, log2I_in_gga(X1, s(X2), X3))
LOG2I_IN_GGA(s(s(X1)), X2, X3) → LOG2I_IN_GGA(X1, s(X2), X3)
LOG2I_IN_GGA(0, s(X1), X2) → U14_GGA(X1, X2, log2J_in_ga(X1, X2))
LOG2I_IN_GGA(0, s(X1), X2) → LOG2J_IN_GA(X1, X2)
LOG2J_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U27_GA(X1, X2, log2K_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2J_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2K_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2K_IN_GGA(s(s(X1)), X2, X3) → U16_GGA(X1, X2, X3, log2K_in_gga(X1, s(X2), X3))
LOG2K_IN_GGA(s(s(X1)), X2, X3) → LOG2K_IN_GGA(X1, s(X2), X3)
LOG2K_IN_GGA(0, s(X1), X2) → U17_GGA(X1, X2, log2L_in_ga(X1, X2))
LOG2K_IN_GGA(0, s(X1), X2) → LOG2L_IN_GA(X1, X2)
LOG2L_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → U26_GA(X1, X2, log2M_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2L_IN_GA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2M_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2M_IN_GGA(s(s(X1)), X2, X3) → U19_GGA(X1, X2, X3, log2M_in_gga(X1, s(X2), X3))
LOG2M_IN_GGA(s(s(X1)), X2, X3) → LOG2M_IN_GGA(X1, s(X2), X3)
LOG2M_IN_GGA(0, s(X1), X2) → U20_GGA(X1, X2, log2N_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2M_IN_GGA(0, s(X1), X2) → LOG2N_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) → U25_GGA(X1, X2, X3, log2O_in_ggga(X1, s(s(s(s(s(s(s(0))))))), X2, X3))
LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) → LOG2O_IN_GGGA(X1, s(s(s(s(s(s(s(0))))))), X2, X3)
LOG2O_IN_GGGA(s(s(X1)), X2, X3, X4) → U22_GGGA(X1, X2, X3, X4, log2O_in_ggga(X1, s(X2), X3, X4))
LOG2O_IN_GGGA(s(s(X1)), X2, X3, X4) → LOG2O_IN_GGGA(X1, s(X2), X3, X4)
LOG2O_IN_GGGA(0, s(X1), X2, X3) → U23_GGGA(X1, X2, X3, log2N_in_gga(X1, s(X2), X3))
LOG2O_IN_GGGA(0, s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)
LOG2O_IN_GGGA(s(0), s(X1), X2, X3) → U24_GGGA(X1, X2, X3, log2N_in_gga(X1, s(X2), X3))
LOG2O_IN_GGGA(s(0), s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)
LOG2M_IN_GGA(s(0), s(X1), X2) → U21_GGA(X1, X2, log2N_in_gga(X1, s(s(s(s(s(s(s(0))))))), X2))
LOG2M_IN_GGA(s(0), s(X1), X2) → LOG2N_IN_GGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2K_IN_GGA(s(0), s(X1), X2) → U18_GGA(X1, X2, log2L_in_ga(X1, X2))
LOG2K_IN_GGA(s(0), s(X1), X2) → LOG2L_IN_GA(X1, X2)
LOG2I_IN_GGA(s(0), s(X1), X2) → U15_GGA(X1, X2, log2J_in_ga(X1, X2))
LOG2I_IN_GGA(s(0), s(X1), X2) → LOG2J_IN_GA(X1, X2)
LOG2G_IN_GGA(s(0), s(X1), X2) → U12_GGA(X1, X2, log2H_in_ga(X1, X2))
LOG2G_IN_GGA(s(0), s(X1), X2) → LOG2H_IN_GA(X1, X2)
LOG2E_IN_GGA(s(0), s(X1), X2) → U9_GGA(X1, X2, log2F_in_ga(X1, X2))
LOG2E_IN_GGA(s(0), s(X1), X2) → LOG2F_IN_GA(X1, X2)
LOG2C_IN_GGA(s(0), s(X1), X2) → U6_GGA(X1, X2, log2D_in_ga(X1, X2))
LOG2C_IN_GGA(s(0), s(X1), X2) → LOG2D_IN_GA(X1, X2)
LOG2A_IN_GGA(s(0), s(X1), X2) → U3_GGA(X1, X2, log2B_in_ga(X1, X2))
LOG2A_IN_GGA(s(0), s(X1), X2) → LOG2B_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
log2A_in_gga(x1, x2, x3)  =  log2A_in_gga(x1, x2)
0  =  0
log2B_in_ga(x1, x2)  =  log2B_in_ga(x1)
log2C_in_gga(x1, x2, x3)  =  log2C_in_gga(x1, x2)
log2D_in_ga(x1, x2)  =  log2D_in_ga(x1)
log2E_in_gga(x1, x2, x3)  =  log2E_in_gga(x1, x2)
log2F_in_ga(x1, x2)  =  log2F_in_ga(x1)
log2G_in_gga(x1, x2, x3)  =  log2G_in_gga(x1, x2)
log2H_in_ga(x1, x2)  =  log2H_in_ga(x1)
log2I_in_gga(x1, x2, x3)  =  log2I_in_gga(x1, x2)
log2J_in_ga(x1, x2)  =  log2J_in_ga(x1)
log2K_in_gga(x1, x2, x3)  =  log2K_in_gga(x1, x2)
log2L_in_ga(x1, x2)  =  log2L_in_ga(x1)
log2M_in_gga(x1, x2, x3)  =  log2M_in_gga(x1, x2)
log2N_in_gga(x1, x2, x3)  =  log2N_in_gga(x1, x2)
log2O_in_ggga(x1, x2, x3, x4)  =  log2O_in_ggga(x1, x2, x3)
LOG2N40_IN_GA(x1, x2)  =  LOG2N40_IN_GA(x1)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
LOG2A_IN_GGA(x1, x2, x3)  =  LOG2A_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3)  =  U2_GGA(x1, x3)
LOG2B_IN_GA(x1, x2)  =  LOG2B_IN_GA(x1)
U31_GA(x1, x2, x3)  =  U31_GA(x1, x3)
LOG2C_IN_GGA(x1, x2, x3)  =  LOG2C_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
LOG2D_IN_GA(x1, x2)  =  LOG2D_IN_GA(x1)
U30_GA(x1, x2, x3)  =  U30_GA(x1, x3)
LOG2E_IN_GGA(x1, x2, x3)  =  LOG2E_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3)  =  U8_GGA(x1, x3)
LOG2F_IN_GA(x1, x2)  =  LOG2F_IN_GA(x1)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
LOG2G_IN_GGA(x1, x2, x3)  =  LOG2G_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
LOG2H_IN_GA(x1, x2)  =  LOG2H_IN_GA(x1)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
LOG2I_IN_GGA(x1, x2, x3)  =  LOG2I_IN_GGA(x1, x2)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
LOG2J_IN_GA(x1, x2)  =  LOG2J_IN_GA(x1)
U27_GA(x1, x2, x3)  =  U27_GA(x1, x3)
LOG2K_IN_GGA(x1, x2, x3)  =  LOG2K_IN_GGA(x1, x2)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3)  =  U17_GGA(x1, x3)
LOG2L_IN_GA(x1, x2)  =  LOG2L_IN_GA(x1)
U26_GA(x1, x2, x3)  =  U26_GA(x1, x3)
LOG2M_IN_GGA(x1, x2, x3)  =  LOG2M_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3)  =  U20_GGA(x1, x3)
LOG2N_IN_GGA(x1, x2, x3)  =  LOG2N_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
LOG2O_IN_GGGA(x1, x2, x3, x4)  =  LOG2O_IN_GGGA(x1, x2, x3)
U22_GGGA(x1, x2, x3, x4, x5)  =  U22_GGGA(x1, x2, x3, x5)
U23_GGGA(x1, x2, x3, x4)  =  U23_GGGA(x1, x2, x4)
U24_GGGA(x1, x2, x3, x4)  =  U24_GGGA(x1, x2, x4)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
U6_GGA(x1, x2, x3)  =  U6_GGA(x1, x3)
U3_GGA(x1, x2, x3)  =  U3_GGA(x1, x3)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 53 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2, X3) → LOG2O_IN_GGGA(X1, s(s(s(s(s(s(s(0))))))), X2, X3)
LOG2O_IN_GGGA(s(s(X1)), X2, X3, X4) → LOG2O_IN_GGGA(X1, s(X2), X3, X4)
LOG2O_IN_GGGA(0, s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)
LOG2O_IN_GGGA(s(0), s(X1), X2, X3) → LOG2N_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
LOG2N_IN_GGA(x1, x2, x3)  =  LOG2N_IN_GGA(x1, x2)
LOG2O_IN_GGGA(x1, x2, x3, x4)  =  LOG2O_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2O_IN_GGGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2O_IN_GGGA(s(s(X1)), X2, X3) → LOG2O_IN_GGGA(X1, s(X2), X3)
LOG2O_IN_GGGA(0, s(X1), X2) → LOG2N_IN_GGA(X1, s(X2))
LOG2O_IN_GGGA(s(0), s(X1), X2) → LOG2N_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

LOG2N_IN_GGA(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))), X2) → LOG2O_IN_GGGA(X1, s(s(s(s(s(s(s(0))))))), X2)
LOG2O_IN_GGGA(s(s(X1)), X2, X3) → LOG2O_IN_GGGA(X1, s(X2), X3)
LOG2O_IN_GGGA(0, s(X1), X2) → LOG2N_IN_GGA(X1, s(X2))
LOG2O_IN_GGGA(s(0), s(X1), X2) → LOG2N_IN_GGA(X1, s(X2))


Used ordering: Knuth-Bendix order [KBO] with precedence:
0 > s1 > LOG2NINGGA2 > LOG2OINGGGA3

and weight map:

0=1
s_1=1
LOG2N_IN_GGA_2=0
LOG2O_IN_GGGA_3=6

The variable weight is 1

(13) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2M_IN_GGA(s(s(X1)), X2, X3) → LOG2M_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2M_IN_GGA(x1, x2, x3)  =  LOG2M_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2M_IN_GGA(s(s(X1)), X2) → LOG2M_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2M_IN_GGA(s(s(X1)), X2) → LOG2M_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2K_IN_GGA(s(s(X1)), X2, X3) → LOG2K_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2K_IN_GGA(x1, x2, x3)  =  LOG2K_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2K_IN_GGA(s(s(X1)), X2) → LOG2K_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(24) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2K_IN_GGA(s(s(X1)), X2) → LOG2K_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(25) YES

(26) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2I_IN_GGA(s(s(X1)), X2, X3) → LOG2I_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2I_IN_GGA(x1, x2, x3)  =  LOG2I_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(27) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2I_IN_GGA(s(s(X1)), X2) → LOG2I_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(29) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2I_IN_GGA(s(s(X1)), X2) → LOG2I_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(30) YES

(31) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2G_IN_GGA(s(s(X1)), X2, X3) → LOG2G_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2G_IN_GGA(x1, x2, x3)  =  LOG2G_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(32) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(33) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2G_IN_GGA(s(s(X1)), X2) → LOG2G_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(34) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2G_IN_GGA(s(s(X1)), X2) → LOG2G_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(35) YES

(36) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2E_IN_GGA(s(s(X1)), X2, X3) → LOG2E_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2E_IN_GGA(x1, x2, x3)  =  LOG2E_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(37) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2E_IN_GGA(s(s(X1)), X2) → LOG2E_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(39) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2E_IN_GGA(s(s(X1)), X2) → LOG2E_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(40) YES

(41) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2C_IN_GGA(s(s(X1)), X2, X3) → LOG2C_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2C_IN_GGA(x1, x2, x3)  =  LOG2C_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(42) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2C_IN_GGA(s(s(X1)), X2) → LOG2C_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(44) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2C_IN_GGA(s(s(X1)), X2) → LOG2C_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(45) YES

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LOG2A_IN_GGA(s(s(X1)), X2, X3) → LOG2A_IN_GGA(X1, s(X2), X3)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LOG2A_IN_GGA(x1, x2, x3)  =  LOG2A_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LOG2A_IN_GGA(s(s(X1)), X2) → LOG2A_IN_GGA(X1, s(X2))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LOG2A_IN_GGA(s(s(X1)), X2) → LOG2A_IN_GGA(X1, s(X2))
    The graph contains the following edges 1 > 1

(50) YES